A:MsgA, b:Id, s, s0:A.state.
ma-frame-compat(A;A)
 b in dom(A.pre)
 (v:A.da(locl(b)).
 (A.pre(b,s,v)  A.pre(b,x.if A:locl(b) may not read x s0(x) else s(x) fi,v)) 

latex

Definitions

b, x:A. B(x), Id, t  T, Knd, type List, x.A(x), x. t(x), Top, a:A fp B(a), x:AB(x), f(a), IdDeq, Type, f(x)?z, locl(a), P  Q, f(x), KindDeq, deq-member(eq;x;L), b, x  dom(f), p  q, if b t else f fi, P  Q, s = t, Prop, A, left+right, P  Q, x:AB(x), IdLnk, P & Q, z != f(x)  P(a;z), State(ds), M.ds(x), xdom(f). v=f(x)   P(x;v), (s1  s2 mod x), M.da(a), M.state, M.rframe(A.sends tfL of k on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), ma-frame-compat(A;B), M:k may not read x, Valtype(da;k), a in dom(M.pre), M.pre(a,s,v), MsgA, P  Q, a = b, list_accum(x,a.f(x;a);y;l), xL. P(x), nil, <a,b>, car.cdr, {T}, (x  l), false, , Unit, eqof(d), p  q, False, True, T, {x:A| B(x) }, 1of(t), Dec(P), nat-deq-aux, NatDeq, atom-deq-aux, AtomDeq, #$n, a<b, Void, AB, , , Atom, prod-deq(A;B;a;b), proddeq(a;b), product-deq(A;B;a;b), SQType(T), s ~ t, x,y. t(x;y)

Lemmas

list accum wf, Id sq, all functionality wrt iff, implies functionality wrt iff, decidable assert, pi1 wf, assert of bor, or functionality wrt iff, squash wf, true wf, bnot thru bor, assert of band, and functionality wrt iff, assert-deq-member, not functionality wrt iff, assert-eq-id, bor wf, eqof wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bfalse wf, eq id wf, l member wf, cons member, l all wf, ma-pre wf, ma-da wf, ma-has-pre wf, ma-frame-compat wf, ma-st wf, msga wf, ma-no-read wf, ma-ds wf, assert wf, not wf, iff wf, ifthenelse wf, band wf, fpf-dom wf, bnot wf, deq-member wf, Kind-deq wf, fpf-ap wf, locl wf, fpf-cap wf, id-deq wf, top wf, fpf-trivial-subtype-top, Knd wf, Id wf